| 1: | app(nil,YS) | → YS | |
| 2: | app(cons(X,XS),YS) | → cons(X,n__app(activate(XS),YS)) | |
| 3: | from(X) | → cons(X,n__from(s(X))) | |
| 4: | zWadr(nil,YS) | → nil | |
| 5: | zWadr(XS,nil) | → nil | |
| 6: | zWadr(cons(X,XS),cons(Y,YS)) | → cons(app(Y,cons(X,n__nil)),n__zWadr(activate(XS),activate(YS))) | |
| 7: | prefix(L) | → cons(nil,n__zWadr(L,prefix(L))) | |
| 8: | app(X1,X2) | → n__app(X1,X2) | |
| 9: | from(X) | → n__from(X) | |
| 10: | nil | → n__nil | |
| 11: | zWadr(X1,X2) | → n__zWadr(X1,X2) | |
| 12: | activate(n__app(X1,X2)) | → app(X1,X2) | |
| 13: | activate(n__from(X)) | → from(X) | |
| 14: | activate(n__nil) | → nil | |
| 15: | activate(n__zWadr(X1,X2)) | → zWadr(X1,X2) | |
| 16: | activate(X) | → X | |
| 17: | APP(cons(X,XS),YS) | → ACTIVATE(XS) | |
| 18: | ZWADR(cons(X,XS),cons(Y,YS)) | → APP(Y,cons(X,n__nil)) | |
| 19: | ZWADR(cons(X,XS),cons(Y,YS)) | → ACTIVATE(XS) | |
| 20: | ZWADR(cons(X,XS),cons(Y,YS)) | → ACTIVATE(YS) | |
| 21: | PREFIX(L) | → NIL | |
| 22: | PREFIX(L) | → PREFIX(L) | |
| 23: | ACTIVATE(n__app(X1,X2)) | → APP(X1,X2) | |
| 24: | ACTIVATE(n__from(X)) | → FROM(X) | |
| 25: | ACTIVATE(n__nil) | → NIL | |
| 26: | ACTIVATE(n__zWadr(X1,X2)) | → ZWADR(X1,X2) | |